M:MsgA. Feasible(M)  (l:IdLnk, tg:Id. AtomFree(Type;M.dout(l,tg))) 

latex

Definitions	t  T, x:A. B(x), rcv(l,tg), P  Q, xdom(f). v=f(x)   P(x;v), Void, Type, AtomFree(T;x), P & Q, b, A, b, , s = t, Prop, Knd, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), KindDeq, x  dom(f), x:AB(x), P  Q, Unit, left+right, f(x)?z, Valtype(da;k), M.sframe(k sends <l,tg>), M.frame(k affects x), M.dout(l,tg), MsgA, Feasible(M), IdLnk, Id
Lemmas	Id wf, IdLnk wf, ma-feasible wf, msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf, rcv wf